T:Type, A, B:T List, x, y:T.
x before y  A @ B  x before y  A  x before y  B  (x  A) & (y  B) 

latex

Definitions	x. t(x), as @ bs, False, {T}, P  Q, P  Q, P  Q, P  Q, x before y  l, P & Q, Prop, (x  l), x:A. B(x), t  T
Lemmas	l member wf, l before wf, nil before, nil member, iff wf, append wf, cons before, or functionality wrt iff, iff functionality wrt iff, all functionality wrt iff, cons member, and functionality wrt iff, member append